翻訳と辞書 Words near each other ・ "O" Is for Outlaw ・ "O"-Jung.Ban.Hap. ・ "Ode-to-Napoleon" hexachord ・ "Oh Yeah!" Live ・ "Our Contemporary" regional art exhibition (Leningrad, 1975) ・ "P" Is for Peril ・ "Pimpernel" Smith ・ "Polish death camp" controversy ・ "Pro knigi" ("About books") ・ "Prosopa" Greek Television Awards ・ "Pussy Cats" Starring the Walkmen ・ "Q" Is for Quarry ・ "R" Is for Ricochet ・ "R" The King (2016 film) ・ "Rags" Ragland ・ ! (album) ・ ! (disambiguation) ・ !! ・ !!! ・ !!! (album) ・ !!Destroy-Oh-Boy!! ・ !Action Pact! ・ !Arriba! La Pachanga ・ !Hero ・ !Hero (album) ・ !Kung language ・ !Oka Tokat ・ !PAUS3 ・ !T.O.O.H.! ・ !Women Art Revolution Dictionary Lists mini英和辞書 mini和英辞書 Webster 1913 Latin-English FOLDOC Wikipedia English ウィキペディア

翻訳と辞書　辞書検索 [ 開発暫定版 ] スポンサード リンク Mu calculus ： ウィキペディア英語版 Modal μ-calculus In theoretical computer science, the modal μ-calculus (Lμ, Lμ, sometimes just μ-calculus, although this can have a more general meaning) is an extension of propositional modal logic (with many modalities) by adding a least fixpoint operator μ and a greatest fixpoint operator $\backslash nu$, thus a fixed-point logic. The (propositional, modal) μ-calculus originates with Dana Scott and Jaco de Bakker,〔Kozen p. 333.〕 and was further developed by Dexter Kozen into the version most used nowadays. It is used to describe properties of labelled transition systems and for verifying these properties. Many temporal logics can be encoded in the μ-calculus, including CTL * and its widely used fragments—linear temporal logic and computational tree logic.〔Clarke p.108, Theorem 6; Emerson p. 196〕 An algebraic view is to see it as an algebra of monotonic functions over a complete lattice, with operators consisting of functional composition plus the least and greatest fixed point operators; from this viewpoint, the modal μ-calculus is over the lattice of a power set algebra.〔Arnold and Niwiński, pp. viii-x and chapter 6〕 The game semantics of μ-calculus is related to two-player games with perfect information, particularly infinite parity games.〔Arnold and Niwiński, pp. viii-x and chapter 4〕 == Syntax == Let ''P'' (propositions) and ''A'' (actions) be two finite sets of symbols, and let ''V'' be a countably infinite set of variables. The set of formulas of (propositional, modal) μ-calculus is defined as follows: * each proposition and each variable is a formula; * if $\backslash phi$ and $\backslash psi$ are formulas, then $\backslash phi\; \backslash wedge\; \backslash psi$ is a formula. * if $\backslash phi$ is a formula, then $\backslash neg\; \backslash phi$ is a formula; * if $\backslash phi$ is a formula and $a$ is an action, then $()\; \backslash phi$ is a formula;(pronounced either: $a$ box $\backslash phi$ or after $a$ necessarily $\backslash phi$) * if $\backslash phi$ is a formula and $Z$ a variable, then $\backslash nu\; Z.\; \backslash phi$ is a formula, provided that every free occurrence of $Z$ in $\backslash phi$ occurs positively, i.e. within the scope of an even number of negations. (The notions of free and bound variables are as usual, where $\backslash nu$ is the only binding operator.) Given the above definitions, we can enrich the syntax with: * $\backslash phi\; \backslash lor\; \backslash psi$ meaning $\backslash neg\; (\backslash neg\; \backslash phi\; \backslash land\; \backslash neg\; \backslash psi)$ * $\backslash langle\; a\; \backslash rangle\; \backslash phi$ (pronounced either: $a$ diamond $\backslash phi$ or after $a$ possibly $\backslash phi$) meaning $\backslash neg\; ()\; \backslash neg\; \backslash phi$ * $\backslash mu\; Z.\; \backslash phi$ means $\backslash neg\; \backslash nu\; Z.\; \backslash neg\; \backslash phi\; (Z)$, where $\backslash phi\; (Z)$ means substituting $\backslash neg\; Z$ for ''Z'' in all free occurrences of ''Z'' in $\backslash phi$. The first two formulas are the familiar ones from the classical propositional calculus and respectively the minimal multimodal logic K. The notation $\backslash mu\; Z.\; \backslash phi$ (and its dual) are inspired from the lambda calculus; the intent is to denote the least (and respectively greatest) fixed point of the expression $\backslash phi$ where the "minimization" (and respectively "maximization") are in the variable ''Z'', much like in lambda calculus $\backslash lambda\; Z.\; \backslash phi$ is a function with formula $\backslash phi$ in bound variable ''Z'';〔Arnold and Niwiński, p. 14〕 see the denotational semantics below for details. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Modal μ-calculus」の詳細全文を読む スポンサード リンク 翻訳と辞書 : 翻訳のためのインターネットリソース Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.